w-machine-constraint(w)
== i:Id.
== let Choose,Trans,Send = w-machine(w;i) in 
== t:.
== ((isnull(a(i;t))))
==  ((x.s(i;t+1).x) = (x,q. Trans(kind(a(i;t)),val(a(i;t)),x.s(i;t).x,x,q + 1))
==  & ((islocal(kind(a(i;t))))
==  & ( (x:
==  & ( (((isl(Choose(act(kind(a(i;t))),x,x.s(i;t).x(0))))
==  & ( (c (val(a(i;t)) = outl(Choose(act(kind(a(i;t))),x,x.s(i;t).x(0)))))))
==  & m(i;t) = Send(kind(a(i;t)),val(a(i;t)),x.s(i;t).x(0))) 

latex

---

clarification:

w-machine-constraint(w)
== i:Id.
== let Choose,Trans,Send = w-machine(w;i) in 
== t:.
== ((w-isnull(w; w-a(w; i; t))))
==  ((x.w-s(w; i; (t+1); x))
==  (=
==  ((x,q. Trans(w-kind(w; w-a(w; i; t)),w-val(w; w-a(w; i; t)),x.w-s(w; i; t; x),x,q + 1))
==  ( x:Idw-vartype(w; i; x)
==  & ((islocal(w-kind(w; w-a(w; i; t))))
==  & ( (x:
==  & ( (((isl(Choose(act(w-kind(w; w-a(w; i; t))),x,x.w-s(w; i; t; x)(0))))
==  & ( (c (w-val(w; w-a(w; i; t))
==  & ( (c (=
==  & ( (c (outl(Choose(act(w-kind(w; w-a(w; i; t))),x,x.w-s(w; i; t; x)(0)))
==  & ( (c ( w-valtype(w; i; w-a(w; i; t))))))
==  & w-m(w; i; t)
==  & =
==  & Send(w-kind(w; w-a(w; i; t)),w-val(w; w-a(w; i; t)),x.w-s(w; i; t; x)(0))
==  &  (Msg(w.M) List)) 

latex

Definitions	let x,y,z = a in t(x;y;z), w-machine(w;i), x:A. B(x), A, isnull(a), Id, x:AB(x), , vartype(i;x), n+m, r + s, P & Q, P  Q, islocal(k), x:A. B(x), , A c B, b, isl(x), valtype(i;a), outl(x), act(k), s = t, type List, Msg(M), w.M, m(i;t), kind(a), val(a), a(i;t), x.A(x), f(a), s(i;t).x, #$n
FDL editor aliases	w-machine-constraint